module traveldream

sig Stringa {}
sig Password{}//entità vuota per le password
sig Mail{}//entità vuota per le email
sig CodiceVolo{}////entità vuota per il codice dei voli
sig CodiceAeroporto{}////entità vuota per il codice degli Aeroporti
//signature per città, o almeno quella più vicina
sig Citta {
	nome : Stringa
}

//timestamp per gestione data e ora.per comodità modellato come intero
sig DataOra {
	time : Int
}{ time >0} 

//creato istanza aeroporto dove uso codice aeroporto (es. malpensa MXP) e città
sig Aeroporto {
	codice : one CodiceAeroporto,
	citta : one Citta
}

//signature per cliente.comprende l'insieme di pacchetti prenotati
sig Cliente {
	email : one Mail,
	password : one Password,
	pacchetti : set Pacchetto
}

//signature per impiegato
sig Impiegato {
	email : one Mail,
	password : one Password,
    token:one Password //stringa di riconoscimento dell'impiegato
}

//signature per pacchetto.si intende il pacchetto già prenotato e modificato.
sig Pacchetto {
	destinazione : one Citta,
	voloAndata : one Volo,
	voloRitorno : one Volo,
	escursione : set Escursione,//l'escursione non è obbligatoria
	hotel : one Hotel,
    prezzotot:one Int,
    numpersone:one Int
}{prezzotot>0}


sig Volo {
	codiceVolo : one CodiceVolo,	
	luogoPartenza : one Aeroporto,
	luogoArrivo : one Aeroporto,
    postirimanenti:one Int,
    prezzosingolo:one Int,
	data : one DataOra
} 

sig Hotel {
	nome: one Stringa,
	citta : one Citta,
    postirimanenti:one Int,
    prezzosingolo:one Int,
	dataPrenotazione : one DataOra,
}

sig Escursione {
	inizio : one DataOra,
	luogo : one Citta,
    prezzosingolo:one Int,
    postirimanenti:one Int
}

//facts per evitare di avere account ripetuti
fact noAccountRipetuti {
	no disj a,b : Impiegato | a.email = b.email
	no disj a,b : Cliente | a.email = b.email
	no disj a : Impiegato, b : Cliente | a.email = b.email 
}

assert A_noAccountRipetuti {
	no disj a,b : Impiegato | a.email = b.email
	no disj a,b : Cliente | a.email = b.email
	no disj a : Impiegato, b : Cliente | a.email = b.email 
}

check A_noAccountRipetuti

//no aeroporti uguali
fact noAeroportoUguale {
	no disj a,b : Aeroporto | a.codice = b.codice
}

assert A_noAeroportoUguale {
	no disj a,b : Aeroporto | a.codice = b.codice
}

check A_noAeroportoUguale

//no voli uguali
fact noVoloUguale {
	no disj a,b : Volo | a.luogoArrivo.codice = b.luogoArrivo.codice //codice aeroporto diverso
	no disj a,b : Volo | a.luogoPartenza.codice = b.luogoPartenza.codice	
	no disj a,b : Volo | a.codiceVolo = b.codiceVolo
}

assert A_noVoloUguale {
	no disj a,b : Volo | a.luogoArrivo.codice = b.luogoArrivo.codice //codice aeroporto diverso
	no disj a,b : Volo | a.luogoPartenza.codice = b.luogoPartenza.codice	
	no disj a,b : Volo | a.codiceVolo = b.codiceVolo
}

check A_noVoloUguale

//no escursione uguale

fact noEscursioneUguale {
	no disj a,b : Escursione | a.inizio = b.inizio
	no disj a,b : Escursione | a.luogo = b.luogo
}

assert A_noEscursioneUguale {
	no disj a,b : Escursione | a.inizio = b.inizio
	no disj a,b : Escursione | a.luogo = b.luogo
}

check A_noEscursioneUguale

//no hotel uguale

fact noHotelUguale {
	no disj a,b : Hotel | a.nome = b.nome
	no disj a,b : Hotel | a.citta = b.citta
}

assert A_noHotelUguale {
	no disj a,b : Hotel | a.nome = b.nome
	no disj a,b : Hotel | a.citta = b.citta
}

check A_noHotelUguale
	

fact voloCorretto{
  all p:Pacchetto | p.voloAndata.luogoArrivo.citta=p.destinazione

}

assert A_voloCorretto{
  all p:Pacchetto | p.voloAndata.luogoArrivo.citta=p.destinazione

}
check A_voloCorretto

fact voliPossibili{
all p:Pacchetto | p.voloRitorno.data.time > p.voloAndata.data.time 
}

assert A_voliPossibili{
all p:Pacchetto | p.voloRitorno.data.time > p.voloAndata.data.time 
}
check A_voliPossibili


fact hotelCorretto{
all p:Pacchetto | p.destinazione=p.hotel.citta 
}

assert A_hotelCorretto{
all p:Pacchetto | p.destinazione=p.hotel.citta 
}
check A_hotelCorretto


fact escursioneCorretta{
all p:Pacchetto | p.escursione.luogo=p.destinazione
}

assert A_escursioneCorretta{
all p:Pacchetto | p.escursione.luogo=p.destinazione
}
check A_escursioneCorretta

fact dispHotel{
all p:Pacchetto | p.hotel.postirimanenti >= p.numpersone 
}

assert A_dispHotel{
all p:Pacchetto | p.hotel.postirimanenti >= p.numpersone 
}
check A_dispHotel



pred show{
	#Cliente = 2
    #Pacchetto=2
}

run show

pred showPacchetti {
	#Pacchetto = 3
}

run showPacchetti
	 

//parte del sistema
sig Sistema{
escursioni:set Escursione,
hotel:set Hotel,
voli:set Volo
}


pred aggiungiVolo[s,s':Sistema,I:Impiegato,v:Volo]{
!(v in s.voli) implies s'.voli=s.voli+ v
}
run aggiungiVolo

pred cancellaEscursione[s,s':Sistema,I:Impiegato,e:Escursione]{
(e in s.escursioni && no p:Pacchetto | e in p.escursione) implies s'.escursioni=s.escursioni-e
}
run cancellaEscursione
